OMon == {g:AbMon| Linorder(|g|;x,y.(x  y))}  

latex

---

clarification:

OMon{i} == {g:AbMon{i}| Linorder(|g|;x,y.(x (g) y))}  

latex

Up	groups 1
Wellformedness Lemmas	omon wf
Definitions	AbMon, Linorder(T;x,y.R(x;y)), |g|, b, x f y,